(CSYM AV00) 
(THVSETQ (THV ANS) (LIST (LIST (QUOTE THV) (GENSYM)))) 
(THVSET (CAR (THV ANS)) NIL) 


(THVSETQ (THV WF) NIL) 
(THVSETQ (THV GCTR) 0) 
(THVSETQ (THV ULS) T) 
(THVSETQ (THV UF) NIL) 
(THVSETQ (THV XN) 0) 
(THVSETQ (THV ZN) 0) 
(THVSETQ (THV YN) 0) 
(THVSETQ (THV COMMENTLIST) NIL) 
(THVSETQ (THV PLANL) NIL) 
(THVSETQ (THV ASSL) NIL) 
(THVSETQ (THV PASSUM) NIL) 
(SETQ GTEMP NIL) 
(SETQ CT NIL) 
(SETQ BTSW NIL) 
(THVSETQ (THV DG) NIL) 
(SETQ AL NIL) 
(SETQ AN 0) 
(SETQ SRULES (QUOTE NIL)) 
(SETQ SSW NIL) 
(SETQ FIFOL NIL) 
(SETQ LIFOL NIL) 
(SETQ SN 0) 
(SETQ PN 0) 
(SETQ READY NIL) 
(SETQ UNCERTLIST NIL) 
(THVSETQ (THV DBLITS) NIL) 
(THVSETQ (THV ASSERTLITS) NIL) 
(THVSETQ (THV WASSERTLITS) NIL) 
(SETQ JOINCOND NIL) 
(THVSETQ (THV PROCLIST) NIL) 
(THVSETQ (THV PROCDATA) NIL) 


(THASSERT (ISVAR X0)) 
(THASSERT (VFACT (1) (1) R)) 
(THASSERT (INTEGER N)) 


(THVSETQ (THV CFACTARGS) NIL) 
(THVSETQ (THV CFACTINST) NIL) 

(DEFPROP CFACTGREMLIN (THERASING (V1 V2) (CFACT (THV V1) (THV V2) R) (THCOND ((MEMBER (THV CFACTINST) (THV CFACT~
ARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT CFACTGREMLIN) 

(THVSETQ (THV NCFACTARGS) NIL) 
(THVSETQ (THV NCFACTINST) NIL) 

(DEFPROP NCFACTGREMLIN (THERASING (V1 V2) (NCFACT (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NCFACTINST) (THV NC~
FACTARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NCFACTGREMLIN) 

(THVSETQ (THV =ARGS) NIL) 
(THVSETQ (THV =INST) NIL) 

(DEFPROP =GREMLIN (THERASING (V1 V2) (= (THV V1) (THV V2) R) (THCOND ((MEMBER (THV =INST) (THV =ARGS)) (THASSERT~
 (WRONG PATH))))) THEOREM) 

(THASSERT =GREMLIN) 

(THVSETQ (THV N=ARGS) NIL) 
(THVSETQ (THV N=INST) NIL) 

(DEFPROP N=GREMLIN (THERASING (V1 V2) (N= (THV V1) (THV V2) R) (THCOND ((MEMBER (THV N=INST) (THV N=ARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM) 

(THASSERT N=GREMLIN) 

(THVSETQ (THV CARGS) NIL) 
(THVSETQ (THV CINST) NIL) 

(DEFPROP CGREMLIN (THERASING (V1 V2) (C (THV V1) (THV V2) R) (THCOND ((MEMBER (THV CINST) (THV CARGS)) (THASSERT~
 (WRONG PATH))))) THEOREM) 

(THASSERT CGREMLIN) 

(THVSETQ (THV NCARGS) NIL) 
(THVSETQ (THV NCINST) NIL) 

(DEFPROP NCGREMLIN (THERASING (V1 V2) (NC (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NCINST) (THV NCARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM) 

(THASSERT NCGREMLIN) 

(THVSETQ (THV CPRODARGS) NIL) 
(THVSETQ (THV CPRODINST) NIL) 

(DEFPROP CPRODGREMLIN (THERASING (V1 V2 V3) (CPROD (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV CPRODINST~
) (THV CPRODARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT CPRODGREMLIN) 

(THVSETQ (THV NCPRODARGS) NIL) 
(THVSETQ (THV NCPRODINST) NIL) 

(DEFPROP NCPRODGREMLIN (THERASING (V1 V2 V3) (NCPROD (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV NCPRODI~
NST) (THV NCPRODARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NCPRODGREMLIN) 

(THVSETQ (THV VFACTARGS) NIL) 
(THVSETQ (THV VFACTINST) NIL) 

(DEFPROP VFACTGREMLIN (THERASING (V1 V2) (VFACT (THV V1) (THV V2) R) (THCOND ((MEMBER (THV VFACTINST) (THV VFACT~
ARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT VFACTGREMLIN) 

(THVSETQ (THV NVFACTARGS) NIL) 
(THVSETQ (THV NVFACTINST) NIL) 

(DEFPROP NVFACTGREMLIN (THERASING (V1 V2) (NVFACT (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NVFACTINST) (THV NV~
FACTARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NVFACTGREMLIN) 

(THVSETQ (THV PRODUCTARGS) NIL) 
(THVSETQ (THV PRODUCTINST) NIL) 

(DEFPROP PRODUCTGREMLIN (THERASING (V1 V2 V3) (PRODUCT (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV PRODU~
CTINST) (THV PRODUCTARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT PRODUCTGREMLIN) 

(THVSETQ (THV NPRODUCTARGS) NIL) 
(THVSETQ (THV NPRODUCTINST) NIL) 

(DEFPROP NPRODUCTGREMLIN (THERASING (V1 V2 V3) (NPRODUCT (THV V1) (THV V2) (THV V3) R) (THCOND ((MEMBER (THV NPR~
ODUCTINST) (THV NPRODUCTARGS)) (THASSERT (WRONG PATH))))) THEOREM) 

(THASSERT NPRODUCTGREMLIN) 



(SETQ RTTAPROD NIL) 
(SETQ RFTAPROD NIL) 
 (DEFPROP TAPROD
	  (THCONSE (CGL V6 V5 V3 (LSTTAPROD (QUOTE (V3 V6 V5))))
		   (PRODUCT (THV V5) (THV V6) (THV V3) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (TREEPATH TAPROD (PRODUCT (THV V5) (THV V6) (THV V3) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 TAPROD))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THOR (THAND (THCOND ((THASVAL (THV V5)) (EQUAL (THV V5) (QUOTE (0))))
					(T (THSETQ (THV V5) (QUOTE (0)))))
				(THCOND ((THASVAL (THV V6)) (EQUAL (THV V6) (QUOTE (0))))
					(T (THSETQ (THV V6) (QUOTE (0))))))
			 (THGOAL (PRODUCT (THEV (LIST (QUOTE MINUS) (THV V5) (THV V3)))
					  (THEV (LIST (QUOTE SUB1) (THV V6)))
					  (THV V3)
 					  R)
				 (THTBF FILTEROP))
			 (CONDSTAT (THV CGL) T))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (SETQ THMS (ADD1 THMS))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RTTAFACT NIL) 
(SETQ RFTAFACT NIL) 
 (DEFPROP TAFACT
	  (THCONSE (CGL V10 V9 (LSTTAFACT (QUOTE (V10 V9))))
		   (VFACT (THV V9) (THV V10) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (TREEPATH TAFACT (VFACT (THV V9) (THV V10) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 TAFACT))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THGOAL (VFACT (THEV (LIST (QUOTE DIV) (THV V9) (THV V10)))
				  (THEV (LIST (QUOTE SUB1) (THV V10)))
 				  R)
			   (THTBF FILTEROP))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (SETQ THMS (ADD1 THMS))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RTTPROD NIL) 
(SETQ RFTPROD NIL) 
 (DEFPROP TPROD
	  (THCONSE (V2 V3 V5 V6 V1 V4 D1 FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST)
		   (CPROD (THV V1) (THV V2) (THV V3) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (TREEPATH TPROD (CPROD (THV V1) (THV V2) (THV V3) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 TPROD))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THSETQ (THV LWF) NIL T T)
		   (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
		   (THSETQ (THV WF) T)
		   (THSETQ (THV LUF) NIL T T)
		   (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
		   (THSET (CAR (THV ANS)) NIL)
		   (NEWVAR (THV V4))
		   (THGOAL (C (THV V4) (0) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V4)))
			    (THSETQ (THV CARGS) (CONS (LIST (THV V4) (QUOTE (0))) (THV CARGS))))
			   (T T))
		   (THGOAL (C (THV V1) (0) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V1)))
			    (THSETQ (THV CARGS) (CONS (LIST (THV V1) (QUOTE (0))) (THV CARGS))))
			   (T T))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
		   (THSET (CAR (THV ANS)) NIL)
		   (THOR T (THFAIL THEOREM))
 		   REP
		   (THGOAL (C (THV V4) (THV V6) R) (THTBF FILTERAX))
		   (THGOAL (C (THV V1) (THV V5) R) (THTBF FILTERAX))
		   (THGOAL (PRODUCT (THV V5) (THV V6) (THV V3) R) (THTBF FILTERAX))
		   (THSETQ (THV INVAR1)
			   (LIST (SIMPLE (LIST (QUOTE PRODUCT) (THV V5) (THV V6) (THV V3) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V1) (THV V5) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V4) (THV V6) (QUOTE R))))
 			   T
 			   T)
		   (THSETQ (THV CTST) (LIST (QUOTE =) (THV V6) (THV V2)))
		   (THOR T (THFAIL THEOREM))
		   (THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
		   (THGOAL (C (THV V4) (THEV (LIST (QUOTE ADD1) (THV V6))) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V4)))
			    (THSETQ (THV CARGS)
				    (CONS (LIST (THV V4) (LIST (QUOTE ADD1) (THV V6))) (THV CARGS))))
			   (T T))
		   (THGOAL (C (THV V1) (THEV (LIST (QUOTE PLUS) (THV V5) (THV V3))) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V1)))
			    (THSETQ (THV CARGS)
				    (CONS (LIST (THV V1) (LIST (QUOTE PLUS) (THV V5) (THV V3))) (THV CARGS))))
			   (T T))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THSETQ (THV V5) (QUOTE THUNASSIGNED))
		   (THSETQ (THV V6) (QUOTE THUNASSIGNED))
		   (THGOAL (C (THV V4) (THV V6) R) (THTBF FILTERAX))
		   (THGOAL (C (THV V1) (THV V5) R) (THTBF FILTERAX))
		   (THGOAL (PRODUCT (THV V5) (THV V6) (THV V3) R) (THTBF FILTERAX))
		   (THCOND ((NOT (THASVAL (THV V3))) (THSETQ (THV V3) (QUOTE ##))) (T T))
		   (THCOND ((NOT (THASVAL (THV V5))) (THSETQ (THV V5) (QUOTE ##))) (T T))
		   (THCOND ((NOT (THASVAL (THV V6))) (THSETQ (THV V6) (QUOTE ##))) (T T))
		   (THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
		   (THSETQ (THV INVAR2)
			   (LIST (SIMPLE (LIST (QUOTE PRODUCT) (THV V5) (THV V6) (THV V3) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V1) (THV V5) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V4) (THV V6) (QUOTE R))))
 			   T
 			   T)
		   (THCOND ((THASVAL (THV FT))
			    (THSETQ (THV NT)
				    (COMPCHANGES (THV INVAR1)
						 (THV INVAR2)
						 (INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS))))))
			   (T
			    (THSETQ (THV FT)
				    (COMPCHANGES (THV INVAR1)
						 (THV INVAR2)
						 (INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS)))))))
		   (THCOND ((AND (NOT (THASVAL (THV NT))) (AMBIG (THV FT))) (THSETQ (THV V5)
										    (QUOTE THUNASSIGNED))
									    (THSETQ (THV V6)
										    (QUOTE THUNASSIGNED))
									    (THSET (CAR (THV ANS)) NIL)
									    (THGO REP))
			   (T T))
		   (SETQ GTEMP
			 (WHILASSEM (THV BP)
				    (THV PB)
				    (COND ((THASVAL (THV NT)) (THV NT)) (T (THV FT)))
				    (THV CTST)))
		   (THSETQ (THV PB) GTEMP T T)
		   (THSETQ (THV PLANL)
			   (CONS (LIST (LIST (QUOTE PROD) (THV V1) (THV V2) (THV V3)) (THV PB)) (THV PLANL)))
		   (THCOND ((THV LWF) (THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS))))
			   (T
			    (THSET (CAR (THV ANS))
				   (APPEND
				    (LIST (LIST (QUOTE ←) (THV V1) (LIST (QUOTE PROD) (THV V2) (THV V3))))))))
		   (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THSETQ (THV CINST) (LIST (THV V1) (THV D1))))
			   (T T))
		   (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THERASE (C (THV V1) (THV D1) R) (THTBF THTRUE)))
			   (T T))
		   (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
		   (THASSERT (C (THV V1) (THEV (LIST (QUOTE PROD) (THV V2) (THV V3))) R))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE C)
						      (THV V1)
						      (LIST (QUOTE PROD) (THV V2) (THV V3))
						      (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE C)
						      (THV V1)
						      (LIST (QUOTE PROD) (THV V2) (THV V3))
						      (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
		   (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
				      (THSETQ (THV BT) NIL T T)
				      (SETQ GANS (REMBT GANS)))
			   (T T))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE CPROD) (THV V1) (THV V2) (THV V3) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE CPROD) (THV V1) (THV V2) (THV V3) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RTTFACT NIL) 
(SETQ RFTFACT NIL) 
 (DEFPROP TFACT
	  (THCONSE (V9 V10 V3 V6 V5 V4 V7 FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST)
		   (CFACT (THV V3) (THV V4) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (TREEPATH TFACT (CFACT (THV V3) (THV V4) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 TFACT))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THSETQ (THV LWF) NIL T T)
		   (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
		   (THSETQ (THV WF) T)
		   (THSETQ (THV LUF) NIL T T)
		   (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
		   (THSET (CAR (THV ANS)) NIL)
		   (THGOAL (INTEGER (THV V4)))
		   (NEWVAR (THV V7))
		   (THGOAL (VFACT (THV V5) (THV V6) R) (THTBF FILTEROP))
		   (THCOND
		    ((THAND (THASVAL (THV V6)) (THASVAL (THV V5)))
		     (THSETQ (THV VFACTARGS) (CONS (LIST (THV V5) (THV V6)) (THV VFACTARGS))))
		    (T T))
		   (THGOAL (C (THV V3) (THV V5) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V5)) (THASVAL (THV V3)))
			    (THSETQ (THV CARGS) (CONS (LIST (THV V3) (THV V5)) (THV CARGS))))
			   (T T))
		   (THGOAL (C (THV V7) (THV V6) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V6)) (THASVAL (THV V7)))
			    (THSETQ (THV CARGS) (CONS (LIST (THV V7) (THV V6)) (THV CARGS))))
			   (T T))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THCOND ((NULL (THV VFACTARGS)) T) (T (THSETQ (THV VFACTARGS) (CDR (THV VFACTARGS)) T T)))
		   (THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
		   (THSET (CAR (THV ANS)) NIL)
		   (THOR T (THFAIL THEOREM))
 		   REP
		   (THGOAL (C (THV V7) (THV V10) R) (THTBF FILTERAX))
		   (THGOAL (C (THV V3) (THV V9) R) (THTBF FILTERAX))
		   (THGOAL (VFACT (THV V9) (THV V10) R) (THTBF FILTERAX))
		   (THSETQ (THV INVAR1)
			   (LIST (SIMPLE (LIST (QUOTE VFACT) (THV V9) (THV V10) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V3) (THV V9) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V7) (THV V10) (QUOTE R))))
 			   T
 			   T)
		   (THSETQ (THV CTST) (LIST (QUOTE >) (THV V10) (THV V4)))
		   (THOR T (THFAIL THEOREM))
		   (THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
		   (THGOAL (C (THV V7) (THEV (LIST (QUOTE ADD1) (THV V10))) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V7)))
			    (THSETQ (THV CARGS)
				    (CONS (LIST (THV V7) (LIST (QUOTE ADD1) (THV V10))) (THV CARGS))))
			   (T T))
		   (THGOAL (CPROD (THV V3) (THV V9) (THEV (LIST (QUOTE ADD1) (THV V10))) R) (THTBF FILTEROP))
		   (THCOND ((THAND (THASVAL (THV V9)) (THASVAL (THV V3)))
			    (THSETQ (THV CARGS)
				    (CONS (LIST (THV V3) (THV V9) (LIST (QUOTE ADD1) (THV V10))) (THV CARGS))))
			   (T T))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
		   (THSETQ (THV V9) (QUOTE THUNASSIGNED))
		   (THSETQ (THV V10) (QUOTE THUNASSIGNED))
		   (THGOAL (C (THV V7) (THV V10) R) (THTBF FILTERAX))
		   (THGOAL (C (THV V3) (THV V9) R) (THTBF FILTERAX))
		   (THGOAL (VFACT (THV V9) (THV V10) R) (THTBF FILTERAX))
		   (THCOND ((NOT (THASVAL (THV V9))) (THSETQ (THV V9) (QUOTE ##))) (T T))
		   (THCOND ((NOT (THASVAL (THV V10))) (THSETQ (THV V10) (QUOTE ##))) (T T))
		   (THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
		   (THSETQ (THV INVAR2)
			   (LIST (SIMPLE (LIST (QUOTE VFACT) (THV V9) (THV V10) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V3) (THV V9) (QUOTE R)))
				 (SIMPLE (LIST (QUOTE C) (THV V7) (THV V10) (QUOTE R))))
 			   T
 			   T)
		   (THCOND ((THASVAL (THV FT))
			    (THSETQ (THV NT)
				    (COMPCHANGES (THV INVAR1)
						 (THV INVAR2)
						 (INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS))))))
			   (T
			    (THSETQ (THV FT)
				    (COMPCHANGES (THV INVAR1)
						 (THV INVAR2)
						 (INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS)))))))
		   (THCOND ((AND (NOT (THASVAL (THV NT))) (AMBIG (THV FT))) (THSETQ (THV V9)
										    (QUOTE THUNASSIGNED))
									    (THSETQ (THV V10)
										    (QUOTE THUNASSIGNED))
									    (THSET (CAR (THV ANS)) NIL)
									    (THGO REP))
			   (T T))
		   (SETQ GTEMP
			 (WHILASSEM (THV BP)
				    (THV PB)
				    (COND ((THASVAL (THV NT)) (THV NT)) (T (THV FT)))
				    (THV CTST)))
		   (THSETQ (THV PB) GTEMP T T)
		   (THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS)))
		   (THASSERT (FACT (THV V3) (THV V4) R))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE FACT) (THV V3) (THV V4) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE FACT) (THV V3) (THV V4) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
		   (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
				      (THSETQ (THV BT) NIL T T)
				      (SETQ GANS (REMBT GANS)))
			   (T T))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE CFACT) (THV V3) (THV V4) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE CFACT) (THV V3) (THV V4) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(SETQ RT← NIL) 
(SETQ RF← NIL) 
 (DEFPROP ←
	  (THCONSE (CGL A1 V1 D1 (LST← (QUOTE (A1 V1))))
		   (C (THV V1) (THV A1) R)
		   (THSETQ (THV LCTR) (THV GCTR))
		   (SETQ THME (ADD1 THME))
		   (THUNIQUE LST←)
		   (TREEPATH ← (C (THV V1) (THV A1) R))
		   (TRACEINFO1)
		   (THOR T (TRACEINFO2 ←))
		   (COND ((TTYIN) (ADVICESYS)) (T T))
		   (THGOAL (ISVAR (THV V1)))
		   (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THSETQ (THV CINST) (LIST (THV V1) (THV D1))))
			   (T T))
		   (THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THERASE (C (THV V1) (THV D1) R) (THTBF THTRUE)))
			   (T T))
		   (THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
		   (THSET (CAR (THV ANS))
			  (CONS (CONS (QUOTE ←) (LIST (THV V1) (THV A1))) (EVAL (CAR (THV ANS)))))
		   (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
		   (SETQ THMS (ADD1 THMS))
		   (THASSERT (C (THV V1) (THV A1) R))
		   (THCOND ((THV ULS)
			    (THSETQ (THV ASSERTLITS)
				    (CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV ASSERTLITS))))
			   (T
			    (THSETQ (THV WASSERTLITS)
				    (CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R))
						(LIST (QUOTE A) (QUOTE A)))
					  (THV WASSERTLITS)))))
		   (PRINT (REVERSE (EVAL (CAR (THV ANS)))))
		   (SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
		   (COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
		   (THDO (TERPRI))
		   (COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
 	  THEOREM)


(THASSERT ←) 


(THASSERT TFACT) 


(THASSERT TPROD) 


(THASSERT TAFACT) 


(THASSERT TAPROD) 
 (DEFPROP RESTOREPROP
	  (LAMBDA NIL
	   (PROG NIL
		 (SETQ STAT T)
		 (SETQ FUNDEFLIST
		       (QUOTE
			((ADD1 (X) (/( X /+ 1 /))) (SUB1 (X) (/( X /- 1 /))) (PLUS (X Y) (/( X /+ Y /))))))
		 (PUTPROP (QUOTE PRODUCT) T (QUOTE DEF))
		 (PUTPROP (QUOTE PRODUCT) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE PRODUCT) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE PRODUCT) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE PRODUCT) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE FACT) T (QUOTE DEF))
		 (PUTPROP (QUOTE FACT) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE FACT) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE FACT) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE FACT) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE VFACT) T (QUOTE DEF))
		 (PUTPROP (QUOTE VFACT) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE VFACT) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE VFACT) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE VFACT) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE CFACT) T (QUOTE DEF))
		 (PUTPROP (QUOTE CFACT) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE CFACT) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE CFACT) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE CFACT) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE CPROD) T (QUOTE DEF))
		 (PUTPROP (QUOTE CPROD) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE CPROD) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE CPROD) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE CPROD) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE =) T (QUOTE DEF))
		 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE =) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE INTEGER) T (QUOTE DEF))
		 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE FLUENT))
		 (PUTPROP (QUOTE >) T (QUOTE DEF))
		 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE UNIQ))
		 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE FLUENT))
		 (PUTPROP (QUOTE C) T (QUOTE DEF))
		 (PUTPROP (QUOTE C) (QUOTE (X *)) (QUOTE UNIQ))
		 (PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE UNCERT))
		 (PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE PARTIAL))
		 (PUTPROP (QUOTE C) (QUOTE T) (QUOTE FLUENT))
		 (PUTPROP (QUOTE TAPROD) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE TAPROD) (QUOTE T) (QUOTE REC))
		 (PUTPROP (QUOTE TAPROD) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE TAPROD) (QUOTE NIL) (QUOTE ARG))
		 (PUTPROP (QUOTE TAPROD) T (QUOTE AX))
		 (PUTPROP (QUOTE TAFACT) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE TAFACT) (QUOTE T) (QUOTE REC))
		 (PUTPROP (QUOTE TAFACT) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE TAFACT) (QUOTE NIL) (QUOTE ARG))
		 (PUTPROP (QUOTE TAFACT) T (QUOTE AX))
		 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE TPROD) (QUOTE NIL) (QUOTE ARG))
		 (PUTPROP (QUOTE TPROD) T (QUOTE ITER))
		 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE TFACT) (QUOTE NIL) (QUOTE ARG))
		 (PUTPROP (QUOTE TFACT) T (QUOTE ITER))
		 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE INEQ))
		 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE REC))
		 (PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE ASSUM))
		 (PUTPROP (QUOTE ←) (QUOTE (V1 A1)) (QUOTE ARG))
		 (PUTPROP (QUOTE ←) T (QUOTE OP))))
 	  EXPR)